ma-single-effect1(x;A;y;B;k;T;f)
== with declarations 
== ds:x : A  y : B
== da:k : T
== effect of k(v) is x := s,v. f(s(x),s(y),v) s v 

latex

---

clarification:

ma-single-effect1(x;A;y;B;k;T;f)
== with declarations 
== ds:fpf-join(IdDeq;x : A;y : B)
== da:k : T
== effect of k(v) is x := s,v. f(s(x),s(y),v) s v 

latex

Definitions	x : v, IdDeq, f  g, with declarations ds:dsda:daeffect of k(v) is x := f s v
FDL editor aliases	ma-single-effect1